Skip to content

Add inversion from weighted#655

Merged
eb8680 merged 9 commits into
staging-weightedfrom
jf-weighted-lifting
May 12, 2026
Merged

Add inversion from weighted#655
eb8680 merged 9 commits into
staging-weightedfrom
jf-weighted-lifting

Conversation

@jfeser
Copy link
Copy Markdown
Contributor

@jfeser jfeser commented May 4, 2026

Depends on #653

@jfeser jfeser changed the base branch from master to staging-weighted May 6, 2026 20:20
@jfeser
Add monoid module (#653)
7c22756 
* add monoid module

* clean up

* fix doctest

* fix

* wip

* remove incorrect rule

* add disjoint set tests and fix bug

* lint

* drop jax monoid defs

* drop incorrect comment

* add assert

* reduce nondeterminism and add assertions

* fix inconsistent stream numbering and missing constant factors
@jfeser jfeser requested a review from eb8680 May 6, 2026 20:27
eb8680
eb8680 reviewed May 6, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@eb8680 eb8680 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Definitely a nice simplification compared to the old version in #639 but can we add this to your hypothesis pipeline or otherwise test it much more extensively? Right now it's hard to say whether it's correct in general.

Comment thread effectful/ops/monoid.py
)


def match_reduce(term: Term) -> tuple | None:
Copy link
Copy Markdown
Contributor

@eb8680 eb8680 May 6, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a very strange function. Surely there's a more comprehensible way to write this, even if it ends up being more verbose.

Copy link
Copy Markdown
Contributor Author

@jfeser jfeser May 6, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed. Unfortunately, I'm not sure how to write this in a way that doesn't enumerate operations. The subclassing relation between operations is implicit, and we want to match all subclasses (and leave open the possibility that new ones could be created).

Comment thread effectful/ops/monoid.py Outdated
Comment thread effectful/ops/monoid.py Outdated
Comment thread tests/test_ops_monoid.py
Comment thread tests/test_ops_syntax.py Outdated
Comment thread tests/test_handlers_llm_provider.py
Comment thread effectful/ops/types.py
@jfeser
Copy link
Copy Markdown
Contributor Author

jfeser commented May 7, 2026 •
edited
Loading

Note: the mapping of reduce over lists conflicts with the reduction rules for cartesian product. In particular, CartesianProduct.reduce([], {i: []}) == CartesianProduct.identity (because reduction over an empty domain is the identity) but the list rule produces []. I've removed the mapping over lists, but we could consider doing something type directed to allow it (and similar rules) when the monoid is not list-typed.

@jfeser jfeser force-pushed the staging-weighted branch from 7c22756 to d558162 Compare May 7, 2026 19:20
@jfeser jfeser force-pushed the jf-weighted-lifting branch from 0daf135 to 1d38f0d Compare May 7, 2026 19:28
@jfeser jfeser mentioned this pull request May 8, 2026
Open
@eb8680 eb8680 merged commit 6987164 into staging-weighted May 12, 2026
29 checks passed
@eb8680 eb8680 deleted the jf-weighted-lifting branch May 12, 2026 18:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eb8680 eb8680 eb8680 approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@jfeser @eb8680